w:World, e:E. FairFifo  rcv?(e)  loc(sender(e)) = source(link(e))  Id 

latex

Definitions	False, t  T, P  Q, True, x:A. B(x), source(l), b, tag(k), lnk(k), act(k), islocal(k), kindcase(k; a.f(a); l,t.g(l;t) ), x:AB(x), left+right, Knd, x:AB(x), s = t, ecase1(e;info;i.f(i);l,e'.g(l;e')), sender(e), loc(e), link(e), w-info(w;e), sender(e), rcv?(e), <a,b>, Id, E, x.A(x), P  Q, P & Q, P  Q, World, FairFifo, loc(e), kind(e)
Lemmas	assert wf, rcv? wf, fair-fifo wf, world wf, w-loc-lemma, sender wf, link wf, Id wf, w-info wf, w-E wf, w-ekind wf, Knd wf, lsrc wf, true wf, false wf